| Definitions | Type, t  T, x:A  B(x), IdLnk,  x:A. B(x), Normal(T), Realizer, type List, nil, "$x", Id,  x.A(x),  x. t(x), x : v, DeclaredType(ds;x), Unit, State(ds), x:A B(x), Void,  x:A. B(x), Top, EqDecider(T), IdDeq, f(x)?z, f(a), car.cdr, <a,b>, locl(a), sends knd(v:T) on l:tagged(g,State(ds),v):dt, rec(x.A(x)), Knd,  , source(l), @loc only events in L change x:T, true, @loc effect knd(v:T) x := f State(ds) v , false, @loc x initially v:T, s.x, s = t, Prop, P   Q, False,  A, A B,  , {x:A| B(x) },  , A & B, P & Q, AtomFree(T;x),  , isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(a), es realizer ind Rsends compseq tag def,  b, R-Feasible(R), inr(x), @loc precondition for a(v:T):P State(ds) v, onceR{$a:ut2, $done:ut2}(i), (x l), hd(l), i<j, ij, l[i], tl(l), {T}, SQType(T), s ~ t, #$n, left+right, P  Q, Dec(P), ||as||,  x:A. B(x), xL. P(x), i j < k, {i..j }, True, b, a:A fp B(a), lnk-decl(l;dt), KindDeq, f  g, P  Q, P Q, a = b, Atom$n, es realizer ind Rframe compseq tag def, i=j, Rsends-T(x1), Rsends-dt(x1), Rsends-l(x1), Rsends-knd(x1), Rsends?(x1), Reffect-T(x1), Reffect-knd(x1), Reffect?(x1), Rrframe-L(x1), Rpre-a(x1), Rpre-ds(x1), Rrframe-x(x1), Rrframe?(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-g(x1), Rsframe-tag(x1), Rsframe-lnk(x1), Rsframe?(x1), Reffect-ds(x1), Raframe-L(x1), Reffect-x(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Rframe-x(x1), Rframe?(x1), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), R-interface-compat(A;B), R-frame-compat(A;B), p = q, R-base-domain(R), Rda(R), Rds(R), R-loc(R), R-has-loc(R;i), es realizer ind Rnone compseq tag def, es realizer ind Rplus compseq tag def, , left right, let x = a in b(x), isrcv(k), if b t else f fi, A || B, f || g, es realizer ind Reffect compseq tag def, es realizer ind Rinit compseq tag def, es realizer ind Rpre compseq tag def, (L), (x,yL.P(x;y)), send_onceR{$done:ut2, $tg:ut2, $b:ut2, $done1:ut2}(T; A; f; l) |
